The present disclosure relates to model checking, in general, and to SAT-based model checking, in particular.
State of the art computerized components are very complex and require extensive quality assurance checks. One of the commonly used techniques is formal verification in which the computerized component is modeled and is examined by a model checker. The model describes all possible behaviors of the computerized component based on inputs from the environment and calculations performed by the computerized component itself. Most components are represented by cycled models in which the state of the component may differ from one cycle to the other. It will be noted that the computerized component may be a software component, firmware component, hardware component or the like. It will be further noted that in some cases the component to be verified may be a business method, user interaction, communication protocol or any other form of activity or computation that may be expressed formally using a model.
A model checker checks that the model holds a predetermined specification property. An exemplary specification property may be that a triggered event is always handled by the component or that a certain variable is never assigned a predetermined value. The specification property may be attributed to one or more cycles. For simplicity, the current disclosure discusses mainly a specification property that is associated to a cycle. However, it should be understood that the disclosed subject matter is not limited to such a specification property. For example, the specification property may be associated with more than one cycle, such as for example, after a flag is raised in a cycle, an alert is issued within a predetermined number of cycles.
One form of model checking utilizes a Bounded Model Checker (BMC). The bounded model checker determines whether the specification property holds for a predetermined number of cycles. A bounded model is a model which has a bounded number of cycles. A bounded model associated with an unbounded model may be determined by truncating behaviors of the model in every cycle that exceeds a predetermined bound. While the BMC may falsify the specification property by determining that in a given one or more cycles the specification property is not held, it cannot prove that the specification is held for the model, as the number of cycles is bounded. The BMC can only provide a proof that the specification is held for every cycle of within the predetermined number of cycles.
One family of BMC engines utilize a SAT solver for solving a Boolean satisfiability problem that is associated with the predetermined number of cycles. The Boolean satisfiability problem is formulated in a Conjunctive Normal Form (CNF) formula.
Although BMC engines are usually faster and more efficient than other types of model checking engines, they are unable to provide a proof that the model holds the specification property in each and every possible behavior. The BMC engines allow only to falsify a specification property by providing a satisfying assignment of the CNF or to provide a proof that given a predetermined bound on the number of cycles, the specification property holds. Many artisans believe that an efficient solution to performing an unbounded model checking may utilize a bounded model checker, such as a BMC that utilizes a SAT solver. It is also believed by many artisans that as a size of a proof is reduced, an efficiency of a method using the proof may increase. Therefore, it is a long felt need to provide for a process, machine or the like for reducing the size of a proof, and for a process, machine or the like for utilizing a SAT solver for performing an unbounded model checking.